/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;
import java.io.File;
import java.io.IOException;
import java.io.LineNumberReader;
import java.io.Reader;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.List;

import alloy.util.CleanupManager;
import alloy.util.Dbg;
import alloy.util.EnvFailureException;
import alloy.util.TmpFiles;

/**
 * BLBackend: Java interface to a backend which solves SAT problems for us
 * This is the generic interface to a backend, which has subclasses for
 * particular backends.
 * Given a {@link BooleanFormula}, can return a satisfying
 * assignment or report that the formula is not satisfiable.
 * Can enumerate and count satisfying assignments for satisfiable formulas.
 */
public abstract class BLBackend {
	// rseater writes:
	// Only implemented by BLSATLab; BLPSolver is never used and may not be up to spec anymore
	// for details, see comment next to the USE_PSOLVER field (below)

    // Possible return values of {@link #solve} and {@link #next}.  These values
    // must be in sync with the same-name C++ constants defined in SatLab/src/solvctrl/SC_SolverControl.hh

    /** Formula unsatisfiable */
    public static final int BL_UNSAT = 0;

    /** Formula satisfiable; {@link #getLastSolution} returns the satisfying Boolean
    assignment. */
    public static final int BL_SAT = 1;

    /** Search unfinished (cancelled) -- not known whether formula is satisfiable */
    public static final int BL_CANCELLED = 2;

    /**
     * Variable ordering of the solver is reported, for use in constructing
     * a {@link alloy.symm symmetry-breaking predicate}.
     */
    public static final int BL_VARORDER = 3;

    /** An error occurred during search. */
    public static final int BL_ERR = 4;

    /** Marks end of a batch of solutions. */
    public static final int BL_ENDBATCH = 5;

    /** Solution count is returned. */
    public static final int BL_SOLCOUNT = 6;

    /** Support enumeration of solutions */
    public static final boolean ENUM_ON = true;
    /** Don't support enumeration of solutions */
    public static final boolean ENUM_OFF = false;

    //
    // Constants for selecting the type of SAT solver
    // run, i.e. what are we asking the SAT solver
    // to do with the formula.  Choices are:
    //

    /** Look for a solution */
    public static final int BL_RUN_SOLVE = 0;

    /** Count solutions */
    public static final int BL_RUN_COUNT = 1;

    /**
     * Gather statistics on which variables are set early in the search,
     * and return the list of such variables.  (Used for trying to get
     * a better symmetry-breaking predicate.)
     */
    public static final int BL_RUN_VARORDER = 2;

    /////
    // coding oddity / relic:
    // this static variable tells you which subtype will be implementing this abstract class
    // with this setting, only BLSATLab (not BLPSolver) can implement it
    private static final boolean USE_PSOLVER = false; // use psolver or satlab
    /** singleton instance */
    private static BLBackend _theInstance;
    
    // static initializer
    static {
    	initSingleton();
    }
    public static void initSingleton() {
    	_theInstance = (USE_PSOLVER ? ((BLBackend) new BLPSolver ()) :
                           ((BLBackend) new BLSATLab ()));
    }
    
    
    /** Result of last {@link #solve} or {@link #next} call:
    one of {@link #BL_UNSAT}, {@link #BL_SAT}, {@link #BL_CANCELLED}, or
    {@link #BL_ERR}. */
    protected int _lastResult;

    /** Satisfying assignment, if {@link #_lastResult} is
    {@link #BL_SAT}; otherwise <code>null</code>.
    Returned by {@link #getLastSolution}. */
    protected boolean[] _lastSolution;

    protected int[] _lastVarOrder;

    /** Solution count returned by the last solution-counting operation. */
    protected BigInteger _lastSolCount;

    protected static String _portFile = null; // only used by BLPSolver but for convenience here

    //////////////
    // Methods //
    ////////////

    public long getLastConvertTime() { return 0; }
    public long getLastSolveTime() { return 0; }

    /** return the singleton instance */
    public static BLBackend getInstance() { return _theInstance; }

    public static void setPortFile (String fname) { _portFile = fname; }
    public static void kill() {
    _theInstance._killProcess();
    }

    {
    // add a cleanup method to kill the solver, if it is running, before
    // quitting java.  ensure that we kill the solver before attempting
    // to delete temporary files -- so that any files that were opened
    // by the solver can be deleted without running into sharing
    // violations.
    CleanupManager.addCleanupMethod(TmpFiles.CLEANUP_ORDER_NUMBER - 1,
                    new Runnable() { public void run() { kill(); } });
    }

    protected abstract void _killProcess();

    /** Whether the given solver can enumerate solutions. */
    public static boolean canEnumerateSolutions(String solverName_) {
    return solverName_.equals("MCHAFF") || solverName_.equals("RELSAT");
    }

    /** Return the result of the last {@link #solve} or {@link #next} call. */
    public static int getLastResult() { return _theInstance._lastResult; }

    /** Return the satisfying assignment generated by the last {@link #solve} or {@link #next}
    call, if {@link #getLastResult} is {@link #BL_SAT}; otherwise, return
    <code>null</code>. */
    public static boolean[] getLastSolution() { return _theInstance._lastSolution; }
    public static int[] getLastVarOrder() { return _theInstance._lastVarOrder; }

    /** Return the solution count obtained by the last solution-counting operation. */
    public static BigInteger getLastSolCount() { return _theInstance._lastSolCount; }

    /**
     * Solve a .sat instance.
     *
     * @return {@link #BL_UNSAT}, {@link #BL_SAT}, {@link #BL_CANCELLED}, or {@link #BL_ERR}.
     *         If {@link #BL_SAT} is returned, {@link #getLastSolution} may be called to
     *         retrieve the satisfying assignment, and {@link #next} may be called to
     *         enumerate subsequent satisfying assignment.
     * @throws EnvFailureException in case of correctable environment failure (e.g. not enough memory)
     */
    public static int solve(BooleanFormula formula_,
                int nvars_, boolean[] dependentVars_,
                String solverName_,
                boolean enum_,
                long randSeed_,
                int runType_,  // BL_RUN_SOLVE/BL_RUN_COUNT/BL_RUN_VARORDER
                File primVarFileHandle_) throws EnvFailureException {
    return _theInstance._solve(formula_, nvars_, dependentVars_,
                   solverName_, enum_, randSeed_, runType_,
                   primVarFileHandle_);
    }

    public static int next() {  return _theInstance._next(); }

    /**
     * Cause a currently running {@link #solve} or {@link #next} to quit immediately,
     * returning {@link #BL_CANCELLED}.
     */
    public void interruptSolver() {
    // call internal method
    _interruptSolver();
    }

    protected abstract void _interruptSolver ();

    /** constructor - we now run the solver process every time */
    protected BLBackend() { }

    /** Check the environment to make sure all the necessary files
    are present, the temporary directory is writeable, etc.
    If there is a problem, returns a {@link String} error message;
    otherwise returns <code>null</code>.   Note that this method
    is virtual (different checks for {@link BLSATLab} and {@link BLPSolver}),
    so it cannot be static. */
    protected String _checkEnvironment() { return null; }

    /** Check the environment to make sure all the necessary files
    are present, the temporary directory is writeable, etc.
    If there is a problem, returns a {@link String} error message;
    otherwise returns <code>null</code>.  */
    public static String checkEnvironment() { return getInstance()._checkEnvironment(); }

    /**
     * Solve a .sat instance.
     *
     * @return {@link #BL_UNSAT}, {@link #BL_SAT}, {@link #BL_CANCELLED}, or {@link #BL_ERR}.
     *         If {@link #BL_SAT} is returned, {@link #getLastSolution} may be called to
     *         retrieve the satisfying assignment, and {@link #next} may be called to
     *         enumerate subsequent satisfying assignment. */
    abstract protected int _solve(BooleanFormula formula_,
                  int nvars_, boolean[] dependentVars_,
                  String solverName_,
                  boolean enum_, long randSeed_,
                  int runType_,  // BL_RUN_SOLVE/BL_RUN_COUNT/BL_RUN_VARORDER
                  File primVarFileHandle_) throws EnvFailureException;

    /** Get next solution, if last solve() returned BL_SAT */
    abstract protected int _next();

    protected static int[] _readVarOrderFrom(LineNumberReader reader_) {
    try {
        _theInstance._lastResult = Integer.parseInt(reader_.readLine());
        List varOrder = null;
        if (_theInstance._lastResult == BL_VARORDER) {
        varOrder = new ArrayList();
        int var = 0;
        do {
            var = Integer.parseInt(reader_.readLine());
            if (var != 0)
            varOrder.add(new Integer(var));
        } while (var!=0);
        }
        reader_.close();
        int[] result = new int[varOrder.size()];
        for (int i=0; i<result.length; i++)
        result[i] = ((Integer)varOrder.get(i)).intValue();
        return _theInstance._lastVarOrder = result;
    } catch (Exception ioe_) {
        Dbg.fatal("error reading variable order: ", ioe_);
        return null;
    }
    }

    protected static BigInteger _readSolCountFrom(LineNumberReader reader_) {
    try {
        _theInstance._lastResult = Integer.parseInt(reader_.readLine());
        Dbg.chk(_theInstance._lastResult == BL_SOLCOUNT);
        _theInstance._lastSolCount = new BigInteger(reader_.readLine());
        reader_.close();
        return _theInstance._lastSolCount;
    } catch (Exception ioe_) {
        Dbg.fatal("error reading solution count: ", ioe_);
        return null;
    }
    }

    /**
     * Read the next solution from the given stream (an opened solution file).
     * Set <code>_theInstance._lastResult</code> and <code>_theInstance_._lastSolution</code>.
     */
    protected static boolean[] _readAssignmentFrom(LineNumberReader solReader_, int nvars_) {
    boolean[] assignment = null;
    try {
        // the assignment is given as a list of variables whose value is true
        _theInstance._lastResult = Integer.parseInt(solReader_.readLine());
        if (_theInstance._lastResult == BL_SAT) {
        assignment = new boolean[nvars_+1];  // initialized to false
        while(true) {
            int trueVar = Integer.parseInt(solReader_.readLine());
            if (trueVar == 0) break;
            // auxiliary variables may have been added during
            // sat2cnf conversion; their values may be given
            // in the solution file, but here we're only
            // interested in values of the boolean variables
            // of the original Boolean formula.
            if (trueVar < assignment.length)
            assignment[trueVar] = true;
        }
        }
    } catch (Exception ioe_) {
        Dbg.fatal("error reading assignment: ", ioe_);
        return null;
    }
    //  for (int i=1; i<assignment.length; i++)
    //      System.out.print(assignment[i] ? "1" : "0");
    //  System.out.println();

    //  BitSet bitSetSol = new BitSet();
    //  for (int i=1; i<assignment.length; i++)
    //      if (assignment[i]) bitSetSol.set(i);
    //  if (solutionsSeen.contains(bitSetSol))
    //      Dbg.info("WARNING: duplicate solution");
    //  else {
    //      solutionsSeen.add(bitSetSol);
    //      Dbg.info("new solution, now have " + solutionsSeen.size());
    //  }

    return _theInstance._lastSolution = assignment;
    }

    //private static Set solutionsSeen = new HashSet();

    /** Read the next integer from a reader */
    private static int _readInt(Reader r_) throws IOException {
    StringBuffer intChars = new StringBuffer();
    // skip non-integer characters
    char c;
    while(true) {
        c = (char)r_.read();
        if (c >= '0' && c <= '9') break;
    }
    intChars.append(c);
    while(true) {
        c = (char)r_.read();
        if (c >= '0' && c <= '9') {
        intChars.append(c);
        }
        else break;
    }
    try {
        return Integer.parseInt(intChars.toString());
    } catch (NumberFormatException nfe_) {
        throw new IOException("Invalid number format");
    }
    }

    protected File _getLastCnfFileHandle() { return null; }
    protected File _getLastSatFileHandle() { return null; }
    protected File _getLastIstFileHandle() { return null; }

    /**
     * Compute the unsatisfiable core of the last analyzed formula (assumed to be
     * unsatisfiable).
     */
    public static BoolStencil computeUnsatCore() { return _theInstance._computeUnsatCore(); }

    /**
     * Compute the unsatisfiable core of the last analyzed formula (assumed to be
     * unsatisfiable).
     */
    protected abstract BoolStencil _computeUnsatCore();

    public static File getLastCnfFileHandle() { return _theInstance._getLastCnfFileHandle(); }
    public static File getLastSatFileHandle() { return _theInstance._getLastSatFileHandle(); }

    /**
     * Return the name of the last template instantiation file (.ist) output by <code>sat2cnf</code>.
     */
    public static File getLastIstFileHandle() { return _theInstance._getLastIstFileHandle(); }
}  // class BLBackend

